\begin{tabbing}
$\forall$${\it es}$:ES, ${\it Cmd}$:Type, ${\it In}$:AbsInterface(${\it Cmd}$), ${\it isupdate}$:(${\it Cmd}$$\rightarrow\mathbb{B}$), ${\it Sys}$, ${\it Out}$:AbsInterface(Top).
\\[0ex](E(${\it In}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]$\Rightarrow$ \=($\forall$$f$:sys{-}antecedent(${\it es}$;${\it Sys}$).\+
\\[0ex]($\forall$$e$:E(${\it In}$). $f$($e$) = $e$ $\in$ E)
\\[0ex]$\Rightarrow$ \=($\forall$${\it chain}$:(E(${\it Sys}$)$\rightarrow$(Id List)).\+
\\[0ex]chain{-}consistent($f$;${\it chain}$)
\\[0ex]$\Rightarrow$ \=($\forall$$x$, $y$:E(${\it Sys}$).\+
\\[0ex]$x$ is $f$$\ast$($y$)
\\[0ex]$\Rightarrow$ \=($\forall$$j$:Id.\+
\\[0ex]loc($x$) $<<$ $j$
\\[0ex]$\Rightarrow$ $j$ $<<$= loc($y$)
\\[0ex]$\Rightarrow$ ($\forall$$i$:Id. loc($x$) $<<$= $i$ $\Rightarrow$ $i$ $<<$ $j$ $\Rightarrow$ cr{-}fails{-}before(${\it es}$; ${\it Sys}$; ${\it chain}$; $i$; $j$))
\\[0ex]$\Rightarrow$ ($\exists$$e$:E(${\it Sys}$). (loc($e$) = $j$ \& $e$ is $f$$\ast$($y$) \& $x$ is $f$$\ast$($e$)))))))
\-\-\-\-
\end{tabbing}